Double-categorical logic in theory and practice

Abstract: Category theory contains a broad array of gadgets out of which to build specialized logics, as explored in categorical logic and programming language theory. Double category theory can organize and systematize the use of these categorical gadgets. In the first part of the talk, I review joint work with Michael Lambert on double theories and their models. Double theories are categorified theories whose models are categories equipped with extra structure. In the second part, I show how this work can be put to practical effect. I describe ongoing work with collaborators at Topos Institute to build CatColab, an interactive environment for formal, interoperable, conceptual modeling. In technical terms, CatColab is a structure editor for models of domain-specific logics, as defined by double theories.

category theory

Audience: researchers in the topic

( video )

Second Virtual Workshop on Double Categories